$\forall$${\it ds}$,${\it ds'}$:fpf(Id; ${\it ltg}$.Type).
\\[0ex]fpf{-}sub(Id; $x$.Type; id{-}deq; ${\it ds}$; ${\it ds'}$) $\Rightarrow$ subtype\_rel(ma{-}state(${\it ds'}$); ma{-}state(${\it ds}$))